YES(O(1),O(1))

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Strict Trs:
  { a(a(x)) -> b(c(x))
  , c(c(x)) -> a(b(x))
  , b(b(x)) -> a(c(x)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

We add following dependency tuples:

Strict DPs:
  { a^#(a(x)) -> c_1(b^#(c(x)), c^#(x))
  , b^#(b(x)) -> c_3(a^#(c(x)), c^#(x))
  , c^#(c(x)) -> c_2(a^#(b(x)), b^#(x)) }

and mark the set of starting terms.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Strict DPs:
  { a^#(a(x)) -> c_1(b^#(c(x)), c^#(x))
  , b^#(b(x)) -> c_3(a^#(c(x)), c^#(x))
  , c^#(c(x)) -> c_2(a^#(b(x)), b^#(x)) }
Weak Trs:
  { a(a(x)) -> b(c(x))
  , c(c(x)) -> a(b(x))
  , b(b(x)) -> a(c(x)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

Consider the dependency graph:

  1: a^#(a(x)) -> c_1(b^#(c(x)), c^#(x))
     -->_2 c^#(c(x)) -> c_2(a^#(b(x)), b^#(x)) :3
     -->_1 b^#(b(x)) -> c_3(a^#(c(x)), c^#(x)) :2
  
  2: b^#(b(x)) -> c_3(a^#(c(x)), c^#(x))
     -->_2 c^#(c(x)) -> c_2(a^#(b(x)), b^#(x)) :3
     -->_1 a^#(a(x)) -> c_1(b^#(c(x)), c^#(x)) :1
  
  3: c^#(c(x)) -> c_2(a^#(b(x)), b^#(x))
     -->_2 b^#(b(x)) -> c_3(a^#(c(x)), c^#(x)) :2
     -->_1 a^#(a(x)) -> c_1(b^#(c(x)), c^#(x)) :1
  

No dependency pair can be employed in a derivation starting from a
marked basic term.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Weak Trs:
  { a(a(x)) -> b(c(x))
  , c(c(x)) -> a(b(x))
  , b(b(x)) -> a(c(x)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

No rule is usable, rules are removed from the input problem.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Rules: Empty
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

Empty rules are trivially bounded

Hurray, we answered YES(O(1),O(1))